es:event_system{i:l}, L:(Id List), del:rationals.
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 (fischer-delay{i:l,
 (fischer-delay{x:ut2,
 (fischer-delay{try:ut2,
 (fischer-delay{taken:ut2,
 (fischer-delay{contending:ut2,
 (fischer-delay{free:ut2,
 (fischer-delay{mine:ut2,
 (fischer-delay{wanted:ut2,
 (fischer-delay{z:ut2}
 (fischer-delay(es; del; L)
 ( prop{i:l}) 

latex

Definitions	False, A  B, A, IdLnk, x:A. B(x), A c B, P  Q, mkid{$x:ut2}, P  Q, (x  l), fischer-delay, prop{i:l}, t  T, P  Q, Id, x:A. B(x), P  Q, l_all(L; T; x.P(x)), es-dtype(es; i; x; T), , b, @e(xv), fischer
Lemmas	event system wf, Id wf, rationals wf, fischer wf, es-sender wf, es-time wf, qadd wf, qless wf, false wf, es-lnk wf, es-tag wf, es-loc wf, es-dtype wf, deq wf, subtype rel self, unchanged-for wf, es-when wf, select wf, length wf1, nat wf